|
The Isabelle theorem prover is an interactive theorem prover, a Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core to ease logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license. ==Example proof== Isabelle allows proofs to be written in two different styles, the procedural and the declarative. Procedural proofs specify a series of tactics or procedures to apply; while reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. Declarative proofs (supported by Isabelle's proof language, Isar), on the other hand, specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans. For example, a declarative proof in Isar that the proof that the square root of two is not rational can be written as follows. sqrt2_not_rational: m n :: nat n_nonzero: sqrt_rat: lowest_terms: .. n_nonzero sqrt_rat simp (auto simp add: power2_eq_square) simp simp eq: .. .. two_is_prime dvd_m: (rule prime_dvd_power_two) k .. eq (auto simp add: power2_eq_square mult_ac) simp .. two_is_prime (rule prime_dvd_power_two) dvd_m (rule gcd_greatest) lowest_terms simp False arith 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Isabelle (proof assistant)」の詳細全文を読む スポンサード リンク
|